Combining data and theory for derivable scientific discovery with AI-Descartes.

Scientists aim to discover meaningful formulae that accurately describe experimental data. Mathematical models of natural phenomena can be manually created from domain knowledge and fitted to data, or, in contrast, created automatically from large datasets with machine-learning algorithms. The problem of incorporating prior knowledge expressed as constraints on the functional form of a learned model has been studied before, while finding models that are consistent with prior knowledge expressed via general logical axioms is an open problem. We develop a method to enable principled derivations of models of natural phenomena from axiomatic knowledge and experimental data by combining logical reasoning with symbolic regression. We demonstrate these concepts for Kepler's third law of planetary motion, Einstein's relativistic time-dilation law, and Langmuir's theory of adsorption. We show we can discover governing laws from few data points when logical reasoning is used to distinguish between candidate formulae having similar error on the data.

Learning to Guide a Saturation-Based Theorem Prover.

Traditional automated theorem provers have relied on manually tuned heuristics to guide how they perform proof search. Recently, however, there has been a surge of interest in the design of learning mechanisms that can be integrated into theorem provers to improve their performance automatically. In this work, we describe TRAIL (Trial Reasoner for AI that Learns), a deep learning-based approach to theorem proving that characterizes core elements of saturation-based theorem proving within a neural framework. TRAIL leverages (a) an effective graph neural network for representing logical formulas, (b) a novel neural representation of the state of a saturation-based theorem prover in terms of processed clauses and available actions, and (c) a novel representation of the inference selection process as an attention-based action policy. We show through a systematic analysis that these components allow TRAIL to significantly outperform previous reinforcement learning-based theorem provers on two standard benchmark datasets (up to 36% more theorems proved). In addition, to the best of our knowledge, TRAIL is the first reinforcement learning-based approach to exceed the performance of a state-of-the-art traditional theorem prover on a standard theorem proving benchmark (solving up to 17% more theorems).

Deceased Donor-initiated Chains: First Report of a Successful Deliberate Case and Its Ethical Implications.

BACKGROUND: It has been suggested that deceased donor kidneys could be used to initiate chains of living donor kidney paired donation, but the potential gains of this practice need to be quantified and the ethical implications must be addressed before it can be implemented. METHODS: The gain of implementing deceased donor-initiated chains was measured with an algorithm, using retrospective data on the pool of incompatible donor/recipient pairs, at a single center. The allocation rules for chain-ending kidneys and the characteristics and quality of the chain-initiating kidney are described. RESULTS: The benefit quantification process showed that, with a pool of 69 kidneys from deceased donors and 16 pairs enrolled in the kidney paired donation program, it was possible to transplant 8 of 16 recipients (50%) over a period of 3 years. After obtaining the approval of the Veneto Regional Authority's Bioethical Committee and the revision of the Italian National Transplant Center's allocation policies, the first successful case was completed. For the recipient (male, aged 53 y), who entered the program for a chain-initiating kidney with a Kidney Donor Risk Index of 0.61 and a Kidney Donor Profile Index of 3%, the waiting time was 4 days. His willing donor (female, aged 53 y) with a Living Kidney Donor Profile Index of 2, donated 2 days later to a chain-ending recipient (male, aged 47 y) who had been on dialysis for 5 years. CONCLUSIONS: This is the first report of a successfully completed, deliberate deceased donor-initiated chain, which was made possible after a thorough assessment of the ethical issues and the impact of allocation policies. This article includes a preliminary efficacy assessment and describes the development of a dedicated algorithm.